(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".


inductive eq_nat  : nat → nat → Prop ≝
  | eq_rif : ∀n. eq_nat n n 
  | eq_trans : ∀n,m,p. eq_nat n m → eq_nat m p → eq_nat n p
  | eq_mio : eq_nat 0 1. (* Impongo questa uguaglianza perché .... non direbbe 
                             sin dall'inizio qual è l'obiettivo? *)
  
  (*
inductive eq_na (n:nat) : nat → Prop ≝
  | eq_rif : eq_na n n 
  | eq_sim : ∀m. eq_na m n → eq_na n m
  | eq_mio : n=0 → eq_na n 1. (*Perchè non posso scriverla così? - simile alla lessequal*)
  *)
  
  (*
  
  (*
PRIMA DIMOSTRAZIONE CHE NON FUNZIONA*)
lemma prova3 : ∀n,m: nat. n≠0  → (eq_nat n m → n=m).
#n #m #i0 #i
inversion i (*Il caso speciale e la riflessività li risolvo facilmente*)
[ #n0 // | | #a destruct lapply i0 * #i0 lapply (i0 (refl ? O)) *] 
(*Ora qui dovrebbe bastare l'induzione ma le ipotesi non sono sufficienti,
almeno non mi sembra*)
*)


(*
(* SECONDA DIMOSTRAZIONE CHE NON FUNZIONA *)

lemma prova2 : ∀n,m: nat.( n≠0) → (eq_nat n m → n=m).
#n #m
#h
#i
elim i // 
(*Qui invece la elim mi dà ottime ipotesi induttive ma non si cura affatto sul tipo
di struttura su cui induce*)
*)


(*  TERZA DIMOSTRAZIONE CHE NON FUNZIONA*)
(*
 
lemma prova3 : ∀n,m: nat. n≠0  → (eq_nat n m → n=m).
#n #m #i0 #i

elim i in i0; (*Uso l'induzione con il pattern, il comportamento è simile alla inversion, mi pare*)
// 
[ | * #a lapply (a (refl ? 0)) * (*Riesco a risolvere il caso speciale perchè ho imposto delle condizioni sull'induzione*)]
(*Ora il caso per cui dovrei avere ipotesi induttive non riesco a risolverlo,
le ipotesi non mi sembrano idonee*)
#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 (*Ho fatto diversi tentativi ma non riesco*)
*)

(*
Per dimostrare il lemma prova3 ci piacerebbe seguire la traccia seguente, per
casi sulla definizione di eq_nat, e per induzione sulla dimensione della dimostrazione 
di eq_nat n m .

Fisso n, ed m.
Assumo 
H1: n ≠ 0,
H2: eq_nat n m.

I casi possibili di H2 sono:
1) H2 perché vale eq_refl, ovvero n coincide con m. Ma questa è la tesi n = m.
2) H2 perché vale eq_trans, ovvero esiste p tale che eq_nat n p e eq_nat p m.
Siccome la derivaszione di eq_nat n p è più corta della derivazione per eq_nat n m
la conclusione n = p è vera proprio perché valgono H1 e eq_nat n p.
Alla conclusione che vale p = m arrivo con gli stessi passi, dato che la derivaszione di 
eq_nat p m è più corta della derivazione per eq_nat n m.
Concludo per transitività di =, dato che n = p e p = m. 
3) H2 perché vale eq_mio 0 1. Quindi, n = 0 e m = 1.
A mano si tende ad dire che il caso è da escludere dato che n = 0 contraddice H1.
Quindi la dimostraziohe è completa.

*) 